T:Type, eq, le:(TT), op:(TTT), id:T, inv:(TT).
IsEqFun(T;eq)
 Assoc(T;op)
 Ident(T;op;id)
 Comm(T;op)
 (<T, eq, le, op, id, inv>  AbMon) 

latex

Up	groups 1
Definitions of Statement	IsMonoid(T;op;id), GrpSig, |g|, =, *, e, Mon, AbMon
Definitions	t  T, P  Q, x:A. B(x), t.2, t.1, *, |g|, AbMon, =, e, P & Q, Mon, GrpSig, IsMonoid(T;op;id),
Lemmas	bool wf, eqfun p wf, assoc wf, ident wf, comm wf, grp op wf, grp car wf, grp eq wf, grp id wf, monoid p wf